package simplytypeddebruijn


/*
 * Usage: substituteterm(value).astop.into(body)
 *
 */
trait TermSubstitutionProvider { self: TermSubstitutionProvider with AbstractSyntax =>

  type partial <: examplepartial
  type topsubst <: exampletopsubst
  
  def substituteterm(v:LTerm):partial
  abstract class examplepartial(v:LTerm){//self : partial =>
    def asTop: topsubst
    override def toString="[? := "+v+"]"
  }
  abstract class exampletopsubst(v:LTerm){//self:topsubst =>
    def intoterm(term:LTerm):LTerm
    override def toString="[top := "+v+"]"
  }
}
